\documentclass{article} 
\usepackage{url} 
\usepackage{manfnt}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb} 
\usepackage{graphicx}
%\usepackage{latexsym}
\usepackage{xcolor} 
%\usepackage{mathrsfs}
\usepackage{amsmath, amsthm}
\usepackage{diagrams}
\usepackage{stmaryrd}


\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[2]{ \{\mu_{#1}\}_{#1 \in #2}} 
\newcommand{\M}[3]{
\{#1_i \mapsto #2_i\}_{i \in #3}} 
\newcommand{\bm}[4]{
\{(#1_i:#2_i) \mapsto #3_i\}_{i \in #4}} 
\newcommand{\bred}[0]{\to_{\beta}} 
\newcommand{\rat}[0]{\rightarrowtail} 
\newcommand{\polym}[1]{\rightarrowtail_{#1}} 
\newcommand{\tyred}[0]{\rightarrowtail_{\tau}} 

\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{statement}{Statement}
\newtheorem{assumption}{Assumption}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\newcommand{\mlstep}[1]{\twoheadrightarrow_{\underline{#1}}}
\newcommand{\lstep}[1]{\to_{\underline{#1}}}
\newcommand{\mstep}[1]{\twoheadrightarrow_{#1}}
\newcommand{\selfstar}[0]{$\mathbf{S}\ $}
\newcommand{\cc}[0]{ $\mathbf{CC}\ $}
\newcommand{\fcc}[0]{ $\mathbf{FCC}\ $}
\newcommand{\fomega}[0]{$\mathbf{F}_{\omega}^{\rho}\ $}
\newcommand{\interp}[1]{\llbracket #1 \rrbracket}
%\newcommand{\lambdabar}{{\mkern0.75mu\mathchar '26\mkern -9.75mu\lambda}}
\makeatletter
\newcommand{\lambdabar}{{\mathchoice
  {\smash@bar\textfont\displaystyle{0.25}{1.2}\lambda}
  {\smash@bar\textfont\textstyle{0.25}{1.2}\lambda}
  {\smash@bar\scriptfont\scriptstyle{0.25}{1.2}\lambda}
  {\smash@bar\scriptscriptfont\scriptscriptstyle{0.25}{1.2}\lambda}
}}
\newcommand{\smash@bar}[4]{%
  \smash{\rlap{\raisebox{-#3\fontdimen5#10}{$\m@th#2\mkern#4mu\mathchar'26$}}}%
}
\makeatother

\newcommand\restr[2]{{% we make the whole thing an ordinary symbol
  \left.\kern-\nulldelimiterspace % automatically resize the bar with \right
  #1 % the function
  \vphantom{\big|} % pretend it's a little taller at normal size
  \right|_{#2} % this is the delimiter
  }}
\newcommand{\tmu}[0]{\restr{\mu}{\mathfrak{X}} }
\newcommand{\tymu}[0]{\restr{\mu}{\mathcal{X}}}
\newarrowfiller{dasheq} {==}{==}{==}{==}
\newarrow {Mapsto} |--->
\newarrow {Line} -----
\newarrow {Implies} ===={=>}
\newarrow {EImplies} {}{dasheq}{}{dasheq}{=>}
\newarrow {Onto} ----{>>}
\newarrow {DashInto} C{dash}{}{dash}{>}
\newarrow {Dashto}{}{dash}{}{dash}{>}
\newarrow {Dashtoo}{}{dash}{}{dash}{>>}


\begin{document}
%\pagestyle{empty}
\title{ $F:$  \selfstar $\to$ \fomega} 
\author{Peng Fu \\
Computer Science, The University of Iowa}
\date{Last edited: \today}


\maketitle \thispagestyle{empty}

\section{System \selfstar}

\subsection{Specifications}
\label{spec}

\noindent \textbf{Conventions}: $x,y, z$ will be used as names for
term variable, $X,Y,Z$ as names for type variable. $t, a, b, c, e$ will be used as meta-variable for any term. $L, N,M$ denotes arbitrary finite non-empty index set. $i,j,k$ denote index variable. $t_1 \equiv t_2$ means the term (denoted by) $t_1$ is $\alpha$-equivalent to $t_2$, and it also expresses meta level definition unfolding. We are working with terms modulo alpha-equivalence. Let $V$ denote the set of term variable, $U$ denote the set of type variable.


\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t' \ | \ \mu t$

\noindent \textit{Types} $T \ ::= $
$\ X \ | \ \Delta X:\kappa.T \ | \ \Pi x:T_1.T_2 \ | \ \forall x:T_1.T_2 \ | \ \iota x.T \ | \ T \ t \ | \ \lambda X.T \ | \ \lambda x.T\ | \ T_1 T_2 \ | \ \mu T$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \xi x:T.\kappa \ | \  \zeta X:\kappa'. \kappa \  | \ \mu \kappa$. 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa\ | \ \Gamma, \tilde{\mu}$

\noindent \textit{Closure} $\mu \ ::= \ \M{x}{t}{N} \cup \M{X}{T}{M}$

\end{definition} 

\begin{definition}[Metalevel Abrieviation]
\

  \noindent \textit{Objects} $o \ ::= \ t \ | \ T \ | \ \kappa$

  \noindent \textit{Reduction Context} $\mathcal{C} \ ::=$

\noindent $ \bullet \ | \ \lambda x.\mathcal{C} \ | \ \mathcal{C} t'\ | \ t \mathcal{C}\ |\ \Delta X:\kappa.\mathcal{C} \ | \ \Pi x:T .\mathcal{C} \ |\ \Pi x:\mathcal{C}.T \ | \  \forall x:T .\mathcal{C} \ |\ \forall x:\mathcal{C}.T \ | \ \lambda X.\mathcal{C} \ | \ \iota x.\mathcal{C} \ | \ T \mathcal{C} \ | \ \mathcal{C} T \ | \ \xi x:\mathcal{C}.\kappa \ | \  \zeta X:\mathcal{C}. \kappa \ | \ \xi x:\kappa.\mathcal{C} \ | \  \zeta X:\kappa. \mathcal{C}$

\end{definition}
\begin{definition}[Well-formed Context]
\

\footnotesize{
\begin{tabular}{llll}
\infer{ \cdot \vdash \mathsf{wf}}{}

&

\infer{ \Gamma, x:T \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash T:*}

&

\infer{ \Gamma, X:\kappa \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash \kappa:\Box}

&
\infer{\Gamma, \tilde{\mu} \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf}
& \Gamma, \tilde{\mu} \vdash \mathsf{ok}}


\end{tabular}
}
\end{definition}

\begin{definition}[Well-formed Kind]
\

\footnotesize{
\begin{tabular}{llll}

\infer{\Gamma \vdash *:\Box}{}

&

\infer{\Gamma \vdash \zeta X:\kappa'.\kappa: \Box}{\Gamma, X:\kappa' \vdash \kappa : \Box & 
\Gamma  \vdash \kappa' : \Box}

&

\infer{\Gamma \vdash \xi x:T.\kappa: \Box}{\Gamma, x:T \vdash \kappa : \Box
& \Gamma \vdash T:*}
&
\infer{\Gamma \vdash \mu \kappa:  \Box}{\Gamma, \tilde{\mu}
\vdash \kappa:\Box & \Gamma, \tilde{\mu} \vdash \mathsf{ok}}




\end{tabular}
}
\end{definition}

\begin{definition}[Kinding]
\

\footnotesize{
\begin{tabular}{lll}
\infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&
\infer{\Gamma \vdash T : \kappa'}{\Gamma \vdash T:
\kappa & \Gamma \vdash \kappa \cong \kappa' & \Gamma \vdash \kappa': \Box}

&
\infer{\Gamma \vdash \Pi x:T_1.T_2 : *}{ \Gamma \vdash T_1 : * &
\Gamma, x: T_1 \vdash T_2 : *}


\\
\\


\infer{\Gamma \vdash \Delta X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : * & \Gamma \vdash \kappa:\Box}

&

\infer{\Gamma \vdash \mu T: \mu \kappa}{\Gamma, \tilde{\mu}
\vdash T:\kappa & \Gamma, \tilde{\mu} \vdash \mathsf{ok}}

&

\infer{\Gamma \vdash \iota x.T : *}{\Gamma, x:\iota x.T \vdash T : *}
\\
\\

\infer{\Gamma \vdash \lambda X.T: \zeta X:\kappa. \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' & \Gamma \vdash \kappa : \Box }

&

\infer{\Gamma \vdash \lambda x.T: \xi x:T'.\kappa}{\Gamma, x:T' \vdash T : \kappa & \Gamma \vdash T':*}

&
\infer{\Gamma \vdash S t: [t/x]\kappa}{\Gamma \vdash S: \xi x:T.\kappa & 
\Gamma \vdash t:T}

\\
\\

\infer{\Gamma \vdash S T: [T/X]\kappa}{\Gamma \vdash S: \zeta X:\kappa'.\kappa & 
\Gamma \vdash T:\kappa'}

&

\infer{\Gamma \vdash \forall x:T_1.T_2 : *}{ \Gamma, x:T_1 \vdash T_2 : * &
\Gamma \vdash T_1 : *}

\end{tabular}
}
\end{definition}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \cong T_2 & \Gamma \vdash T_2:*}

&
\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T & \Gamma \vdash \iota x.T: *}
\\
\\
\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}


&
\infer[\textit{Indx}]{\Gamma \vdash t : \forall x:T_1.T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:* & x \notin \mathsf{FV}(t)}

&
\infer[\textit{Dex}]{\Gamma \vdash t :[t'/x]T_2}{\Gamma
\vdash t: \forall x:T_1.T_2 & \Gamma \vdash t': T_1}

\\
\\

\infer[\textit{Mu}]{\Gamma \vdash {\mu} t: \mu T}{\Gamma, \tilde{\mu}
\vdash t:T &  \Gamma, \tilde{\mu} \vdash \mathsf{ok}}
&

\infer[\textit{Poly}]{\Gamma \vdash  t :\Delta X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T & \Gamma \vdash \kappa:\Box}

&
\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Delta X:\kappa.T 
& \Gamma \vdash T': \kappa}

\\
\\

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : \Pi x:T_1. T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

&
\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t: \Pi x:T_1. T_2 & \Gamma \vdash t': T_1}

\end{tabular}
}
\end{definition}

%% \noindent Let $\cong$ denote $=_o \cup =_{\beta} \cup =_{\mu}$. Let $=$ denotes the reflexive transitive symmetry closure of $\to$. 

\begin{definition}[Closure Reductions]
\

\footnotesize{
\begin{tabular}{lllll}


\infer{\Gamma \vdash \mu t \to_{o} t}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu T \to_{o} T}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu \kappa \to_{o} \kappa}{\mu \in \Gamma}

&

\infer{\Gamma \vdash \mu o \to_{o} \mu o'}{\Gamma, \tilde{\mu} \vdash o \to_{o} o'}

&
\infer{\Gamma \vdash \mathcal{C}[o] \to_{o} \mathcal{C}[o']}{\Gamma \vdash o \to_{o} o'}

\end{tabular}
}

\end{definition}

\noindent \textbf{Note}: Closure reducton is defined for type level only.
\begin{definition}[Beta Reductions]

\

\footnotesize{
\begin{tabular}{llll}


\infer{\Gamma \vdash x \to_{\beta} t}{(x\mapsto t) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{\Gamma \vdash\mu x_i \to_{\beta} \mu t_i}{(x_i \mapsto
t_i) \in \mu}
&

\infer{\Gamma \vdash(\lambda X.T)T' \to_{\beta} [T'/X]T}{}

\\
\\

\infer{\Gamma \vdash(\lambda x.T)t \to_{\beta} [t/x]T}{}

&

\infer{\Gamma \vdash X \to_{\beta} T}{(X\mapsto T) \in \Gamma}

&

\infer{\Gamma \vdash\mu X_i \to_{\beta} \mu T_i}{(X_i \mapsto
T_i) \in \mu}

&

\infer{\Gamma \vdash \mu o \to_{\beta} \mu o'}{\Gamma, \tilde{\mu} \vdash o \to_{\beta} o'  }

\\
\\

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\beta} \mathcal{C}[o']}{\Gamma \vdash o \to_{\beta} o'}


%% \infer{\Gamma \vdash (\lambdabar x.t)\cdot t' \to_{\beta} [\underline{t}'/x]t}{}

\end{tabular}
}
  
\end{definition}

\begin{definition}[Mu Reductions]

\

\footnotesize{
\begin{tabular}{llll}


\infer{ \Gamma \vdash \mu t \to_{\mu} t}{dom(\mu) \#
\mathsf{FV}(t)}

&
\infer{ \Gamma \vdash \mu(\lambda x.t) \to_{\mu} \lambda x.\mu
t}{}

&

\infer{ \Gamma \vdash \mu(t_1 t_2)  \to_{\mu} (\mu t_1 ) (\mu
t_2)}{}

&

\infer{ \Gamma \vdash \mu(T\ T') \to_{\mu} (\mu T)(\mu T')}{}
\\
\\

\infer{ \Gamma \vdash \mu T \to_{\mu} T}{dom(\mu) \#
\mathsf{FV}(T)}

&

\infer{ \Gamma \vdash \mu(\iota x.T) \to_{\mu} \iota x.\mu T}{}

&

\infer{ \Gamma \vdash \mu(\forall x:T_1.T_2) \to_{\mu} \forall x:\mu T_1.\mu T_2}{}

&

\infer{ \Gamma \vdash \mu(\Delta X:\kappa.T) \to_{\mu} \Delta X:\mu \kappa.\mu T}{}

\\

\\

\infer{ \Gamma \vdash \mu(T\ t) \to_{\mu} (\mu T)(\mu t)}{}

&

\infer{ \Gamma \vdash \mu(\lambda X.T) \to_{\mu} \lambda X.\mu T}{}

&

\infer{ \Gamma \vdash \mu(\lambda x.T) \to_{\mu} \lambda x.\mu T}{}

&
\infer{ \Gamma \vdash \mu(\Pi x:T_1.T_2) \to_{\mu} \Pi x:\mu
T_1.\mu T_2}{}


\\
\\

\infer{ \Gamma \vdash \mu \kappa \to_{\mu} \kappa}{dom(\mu) \#
\mathsf{FV}(\kappa)}

&

\infer{ \Gamma \vdash \mu(\xi x:T.\kappa) \to_{\mu} \xi x:\mu
T.\mu \kappa}{}

&

\infer{ \Gamma \vdash \mu(\zeta X:\kappa'.\kappa) \to_{\mu} \zeta X:\mu
\kappa'.\mu \kappa}{}

&

\infer{\Gamma \vdash \mu o \to_{\mu} \mu o'}{\Gamma, \tilde{\mu} \vdash o \to_{\mu} o'}

\\
\\

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\mu} \mathcal{C}[o']}{\Gamma \vdash o \to_{\mu} o'}


\end{tabular}
}  
\end{definition}


\noindent \textbf{Remarks} :

\begin{itemize}
  \item $\Gamma, \tilde{\mu} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\mu} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\mu}}$ and $\{\Gamma, \tilde{\mu} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\mu}}$.
  \item $\cong $ is the reflexive transitive and symmetry closure of $\to_{\beta} \cup \to_o \cup \to_{\mu}$. 
  \item If $\mu$ is $\M{x}{t}{N}\cup \M{X}{T}{M}$, then $\tilde{\mu}$ is $\bm{x}{T}{t}{N} \cup \bm{X}{\kappa}{T}{M}$.

    \item  For $\M{x}{t}{N}$, we
require for any $ 1 \leq i \leq n $, $\mathsf{FV}(t_i) \subseteq dom(\mu) $. For $\M{X}{T}{M}$, we require for any $ 1 \leq i \leq m $, $\mathsf{FV}(T_i) \subseteq dom(\mu)$. 

\end{itemize}

\section{System \fomega}
\begin{definition}[Syntax]

\

\noindent \textit{Terms} $t \ :: = \ x \ | \ \lambda x.t \ | \ t t'\ | \ {\rho} t$

\noindent \textit{Types} $T \ ::= \ X \ | \ \Delta X:\kappa.T \ | \ T_1 \to T_2 \ | \ \lambda X.T \ | \ T_1 T_2 \ | \ {\rho} T$

\noindent \textit{Kinds} $\kappa \ ::= \ * \ | \ \kappa' \to \kappa$ 

\noindent \textit{Context} $\Gamma \ :: = \ \cdot \ | \ \Gamma, x:T \ |  \ \Gamma, X:\kappa \ | \ \Gamma, \tilde{\rho}$ 

\noindent \textit{Closure} $\rho \ ::= \ \M{x}{t}{N}\cup \M{X}{T}{M}$

\end{definition} 


\begin{definition}[Metalevel Abrieviation]
\

\noindent \textit{Objects} $o \ ::= \ t \ | \ T$

  \noindent \textit{Reduction Context} $\mathcal{C} \ ::= \bullet \ | \ \lambda x.\mathcal{C} \ | \ \mathcal{C} t'\ | \ t \mathcal{C}\ | \ \Delta X:\kappa.\mathcal{C} \ | \ T \to \mathcal{C} \ |\ \mathcal{C} \to T \ | \ \lambda X.\mathcal{C} \ | \ T \mathcal{C} \ | \ \mathcal{C} T$

\end{definition}
\begin{definition}[Well-formed Context]
\

\footnotesize{
\begin{tabular}{lll}
\infer{ \cdot \vdash \mathsf{wf}}{}

&

\infer{ \Gamma, x:T \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf} & \Gamma \vdash T:*}

&

\infer{\Gamma, \tilde{\rho} \vdash \mathsf{wf}}{\Gamma \vdash \mathsf{wf}
& \Gamma, \tilde{\rho} \vdash \mathsf{ok}}

\end{tabular}
}
\end{definition}


\begin{definition}[Kinding]
\

\footnotesize{
\begin{tabular}{llll}
\infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&
%% \infer{\Gamma \vdash T : \kappa'}{\Gamma \vdash T:
%% \kappa & \Gamma \vdash \kappa \cong \kappa' & \Gamma \vdash \kappa': \Box}

%% &
\infer{\Gamma \vdash T_1 \to T_2 : *}{ \Gamma \vdash T_1 : * &
\Gamma \vdash T_2 : *}

&
\infer{\Gamma \vdash {\rho} T: \kappa}{\Gamma, \tilde{\rho}
\vdash T:\kappa & \Gamma, \tilde{\rho} \vdash \mathsf{ok}}

&
\infer{\Gamma \vdash \lambda X.T:\kappa\to \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' }

\\
\\

\infer{\Gamma \vdash S T: \kappa}{\Gamma \vdash S: \kappa' \to \kappa & 
\Gamma \vdash T:\kappa'}

&

\infer{\Gamma \vdash \Delta X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : *}

\end{tabular}
}


\end{definition}

\begin{definition}[Typing Rules]
\

\footnotesize{
\begin{tabular}{lll}
    
\infer[\textit{Var}]{\Gamma \vdash x:T}{(x:T) \in \Gamma}

&
\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \cong T_2 & \Gamma \vdash T_2:*}

&

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : T_1 \to T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

\\
\\
\infer[\textit{App}]{\Gamma \vdash t t':T_2}{\Gamma
\vdash t: T_1 \to T_2 & \Gamma \vdash t': T_1}

&

\infer[\textit{Mu}]{\Gamma \vdash {\rho} t:\rho T} {\Gamma, \tilde{\rho}
\vdash t:T &  \Gamma, \tilde{\rho} \vdash \mathsf{ok}}
&

\infer[\textit{Poly}]{\Gamma \vdash  t :\Delta X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T }

\\
\\

\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Delta X:\kappa.T 
& \Gamma \vdash T': \kappa}


\end{tabular}
}

\end{definition}

\begin{definition}[Closure Reductions]
\

\footnotesize{
\begin{tabular}{llll}


\infer{\Gamma \vdash \rho t \to_{o} t}{\rho \in \Gamma}

&

\infer{\Gamma \vdash \rho T \to_{o} T}{\rho \in \Gamma}


&

\infer{\Gamma \vdash \rho o \to_{o} \rho o'}{\Gamma, \tilde{\rho} \vdash o \to_{o} o'}

&

\infer{\Gamma \vdash \mathcal{C}[o] \to_{o} \mathcal{C}[o']}{\Gamma \vdash o \to_{o} o'}

\end{tabular}
}

\end{definition}

\noindent \textbf{Note}: Closure reduction is at type level. 


\begin{definition}[Beta Reductions]

\

\footnotesize{
\begin{tabular}{llll}


\infer{\Gamma \vdash x \to_{\beta} t}{(x\mapsto t) \in \Gamma}

&
\infer{\Gamma \vdash(\lambda x.t)t' \to_{\beta} [t'/x]t}{}

&

\infer{\Gamma \vdash\rho x_i \to_{\beta} \rho t_i}{(x_i \mapsto
t_i) \in \rho}

&

\infer{\Gamma \vdash(\lambda X.T)T' \to_{\beta} [T'/X]T}{}

\\

\\


\infer{\Gamma \vdash X \to_{\beta} T}{(X\mapsto T) \in \Gamma}

&

\infer{\Gamma \vdash\rho X_i \to_{\beta} \rho T_i}{(X_i \mapsto
T_i) \in \rho}

&

\infer{\Gamma \vdash \rho o \to_{\beta} \rho o'}{\Gamma, \tilde{\rho} \vdash o \to_{\beta} o'}

&

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\beta} \mathcal{C}[o']}{\Gamma \vdash o \to_{\beta} o'}

\end{tabular}
}
  
\end{definition}

\begin{definition}[Rho Reductions]

\

\footnotesize{
\begin{tabular}{llll}


\infer{ \Gamma \vdash \rho t \to_{\rho} t}{dom(\rho) \#
\mathsf{FV}(t)}

&
\infer{ \Gamma \vdash \rho(\lambda x.t) \to_{\rho} \lambda x.\rho
t}{}

&

\infer{ \Gamma \vdash \rho(t_1 t_2)  \to_{\rho} (\rho t_1 ) (\rho
t_2)}{}

&

\infer{ \Gamma \vdash \rho(T\ T') \to_{\rho} (\rho T)(\rho T')}{}

\\
\\

\infer{ \Gamma \vdash \rho T \to_{\rho} T}{dom(\rho) \#
\mathsf{FV}(T)}

&

\infer{ \Gamma \vdash \rho(\Delta X:\kappa.T) \to_{\rho} \Delta X:\rho \kappa.\rho T}{}

&

\infer{ \Gamma \vdash \rho(\lambda X.T) \to_{\rho} \lambda X.\rho T}{}

&

\infer{ \Gamma \vdash \rho(T_1 \to T_2) \to_{\rho} \rho T_1\to \rho T_2}{}

\\
\\

\infer{\Gamma \vdash \rho o \to_{\rho} \rho o'}{\Gamma, \tilde{\rho} \vdash o \to_{\rho} o'}

&

\infer{\Gamma \vdash \mathcal{C}[o] \to_{\rho} \mathcal{C}[o']}{\Gamma \vdash o \to_{\rho} o'}


\end{tabular}
}  
\end{definition}

\noindent \textbf{Remarks} :

\begin{itemize}
  \item $\Gamma, \tilde{\rho} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\rho} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\rho}}$ and $\{\Gamma, \tilde{\rho} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\rho}}$.
  \item $\cong $ is the reflexive transitive and symmetry closure of $\to_{\beta} \cup \to_o \cup \to_{\rho}$. 
  \item If $\rho$ is $\M{x}{t}{N}\cup \M{X}{T}{M}$, then $\tilde{\rho}$ is $\bm{x}{T}{t}{N} \cup \bm{X}{\kappa}{T}{M}$.

    \item  For $\M{x}{t}{N}$, we
require for any $ 1 \leq i \leq n $, $\mathsf{FV}(t_i) \subseteq dom(\rho) $. For $\M{X}{T}{M}$, we require for any $ 1 \leq i \leq m $, $\mathsf{FV}(T_i) \subseteq dom(\rho)$. 

\end{itemize}



\section{Erasure}
\begin{definition}
\

$F(*) \ := *$  

$F(\xi x:T.\kappa) \ := F(\kappa)$  

$F(\zeta X:\kappa'.\kappa) \ := F(\kappa') \to F(\kappa)$  

$F(\mu \kappa)\ := F(\kappa)$

$F(X) \ := X$

$F(\iota x.T) \ := F(T)$

$F(\Delta X:\kappa.T) \ := \Delta X:F(\kappa). F(T)$

$F(\Pi x:T_1.T_2) \ :=  F(T_1) \to F(T_2)$

$F(\forall x:T_1.T_2) \ := F(T_2)$

$F(T_1 T_2) \ := F(T_1) F(T_2)$

$F(\lambda X.T) \ := \lambda X. F(T)$

$F(T\ t) \ := F(T)$

$F(\lambda x.T) \ := F(T)$

$F(\mu T) \ := G(\mu) F(T)$

$F(x)\ := x$

$F(\lambda x.t)\ := \lambda x.F(t)$

$F(t t') \ := F(t) F(t')$

$F(\mu t) \ := G(\mu) F(t)$

$G(x_i \mapsto t_i, \mu) \ := x_i \mapsto F(t_i), G(\mu)$  

$G(X_i \mapsto T_i, \mu) \ := X_i \mapsto F(T_i), G(\mu)$  


\end{definition}

\begin{definition}
\

  $F(x:T, \Gamma) \ := x:F(T), F(\Gamma)$

  $F(X:\kappa, \Gamma)\ := X:F(\kappa), F(\Gamma)$

  $F(x:T \mapsto t, \Gamma) \ := x:F(T) \mapsto F(t), F(\Gamma)$

  $F(X:\kappa \mapsto T, \Gamma) \ := X:F(\kappa) \mapsto F(T), F(\Gamma)$
\end{definition}

\noindent \textbf{Conventions}: Let $\mathcal{M}_s, \mathcal{T}_s, \mathcal{K}_s, \Psi$ denote the set of terms, types , kinds and closures in $\mathbf{S}$, let $\mathcal{M}_{\omega},\mathcal{T}_{\omega}, \mathcal{K}_{\omega}, \Theta$ denote the set of terms, types, kinds and closures in \fomega. 

\begin{lemma}
  If $\kappa \in \mathcal{K}_s$, then $F(\kappa) \in \mathcal{K}_{\omega}$.
\end{lemma}
\begin{proof}
  We prove this by induction on the structure of $\kappa$. 
\end{proof}


\begin{lemma}
\

  \begin{enumerate}
  \item If $t \in \mathcal{M}_s$, then $F(t) \in \mathcal{M}_{\omega}$.
  \item If $T \in \mathcal{T}_s$, then $F(T) \in \mathcal{T}_{\omega}$.
  \item If $\mu \in \Psi$, then $G(\mu) \in \Theta$.
  \end{enumerate}
\end{lemma}

\begin{proof}
We prove (1),(2) by induction on struture of $t,T$, we prove (3) by induction on the length
of $\mu$.

\
\begin{enumerate}
\item \noindent \textbf{Base Cases}: $t = x$. Obvious.
\item \noindent \textbf{Base Cases}: $T = X$. Obvious.
\item \noindent \textbf{Base Cases}: Suppose $\mu = x \mapsto t$, then by (1), we know $F(t) \in \mathcal{M}_{\omega}$. So $G(x \mapsto t) \in \Theta$. Suppose
$\mu = X \mapsto T$, then by (2), we know $F(T) \in \mathcal{T}_{\omega}$. So $G(X \mapsto T) \in \Theta$. 
\end{enumerate}

\begin{enumerate}

\item \noindent \textbf{Step Cases}: $t = \mu t'$. Then $F(t) = G(\mu)F(t')$. By (3), we know
that $G(\mu) \in \Theta$. By IH, we know $F(t') \in \mathcal{M}_{\omega}$. So $G(\mu)F(t') \in \mathcal{M}_{\omega}$.

\item \noindent \textbf{Step Cases}: $T = \mu T'$. Then $F(T) = G(\mu)F(T')$. By (3), we know
that $G(\mu) \in \Theta$. By IH, we know $F(T') \in \mathcal{T}_{\omega}$. So $G(\mu)F(T') \in \mathcal{T}_{\omega}$.

\item \noindent \textbf{Step Cases}: Suppose $\mu = x \mapsto t, \mu'$, then by IH, we know $G(\mu') \in \Theta$. By (1), we know that $F(t) \in \mathcal{M}_{\omega}$. So $G(x \mapsto t, \mu') \in \Theta$. Suppose $\mu = X \mapsto T, \mu'$, then by (2), we know $F(T) \in \mathcal{T}_{\omega}$. By IH, we know $G(\mu') \in \Theta$, So $G(X \mapsto T, \mu') \in \Theta$. 
\end{enumerate}
\end{proof}

\noindent \textbf{Remarks}: I believe above argument is valid, but I could not come up with a proper termination metric (to describe the bootstrap inducton on (1),(2)).


\begin{lemma}
\label{subst}
$F(\kappa) \equiv F([t/x]\kappa)$, $F([T/X]\kappa) \equiv F(\kappa)$, $F([t/x]T) \equiv F(T)$ and $F([T'/X]T) \equiv [F(T')/X]F(T)$ and $F([t'/x]t) \equiv [F(t')/x]F(t)$.
\end{lemma}
\begin{proof}
The first two equalities can be proved by induction on structure of $\kappa$(don't forget local property). For the third and fourth ones, by induction on structure of $T$. Of course, one would worry about cases like $\Delta X:\kappa. T$ and $\mu T$, it turns out that the local property of $\mu$ will help us through the second
case; for the first case, we rely on $F(\kappa)$ is a well-defined kind in \fomega.
\end{proof}

\begin{lemma}
\label{kind}
  If $\Gamma \vdash \kappa \cong \kappa'$, then $F(\kappa) \equiv F(\kappa')$.
\end{lemma}
\begin{proof}
  It suffices to show if $\Gamma \vdash \kappa \to_{o,\beta,\mu} \kappa'$, then $F(\kappa) \equiv F(\kappa')$.
So we proceed by induction on derivation of $\Gamma \vdash \kappa \to_{o,\beta,\mu} \kappa'$.
\end{proof}


\begin{lemma}
\label{inj}
  If $\Gamma \vdash T \to_{o,\beta,\mu} T'$, then $F(\Gamma) \vdash F(T) \hookrightarrow_{o,\beta,\mu} F(T')$.
\end{lemma}

\begin{proof}
  By induction on derivation of $\Gamma \vdash T \to_{o,\beta,\mu} T'$. We use lemma \ref{kind},
lemma \ref{subst} above.
\end{proof}

\begin{lemma}
\label{Bij}
  If $\Gamma \vdash t \to_{o,\beta,\mu} t'$, then $F(\Gamma) \vdash F(t) \to_{o,\beta,\mu} F(t')$.
\end{lemma}
\begin{proof}
  By induction on derivation.
\end{proof}
\begin{theorem}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash T:\kappa$, then $F(\Gamma) \vdash F(T):F(\kappa)$.
  \item  If $\Gamma \vdash t:T$, then $F(\Gamma) \vdash F(t):F(T)$.
  \end{enumerate}
\end{theorem}

\begin{proof}
  We prove the conjuction of (1) and (2). By induction on derivation(we only list a few interesting cases). 

\

\noindent \textbf{Base Cases}: 

\

\begin{tabular}{ll}
\infer{\Gamma \vdash X:\kappa}{(X:\kappa) \in \Gamma}

&

\infer{\Gamma \vdash x:T}{(x:T) \in \Gamma}
  
\end{tabular}

\

\noindent Obvious.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \Delta X:\kappa. T : *}{ \Gamma, X:\kappa \vdash T : * & \Gamma \vdash \kappa:\Box}

\

\noindent By IH(1), we know $F(\Gamma), X:F(\kappa) \vdash F(T) : F(*)$. So $F(\Gamma) \vdash \Delta X:F(\kappa). F(T):*$.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \mu T: \mu \kappa}{\Gamma, \tilde{\mu}
\vdash T:\kappa & \Gamma, \tilde{\mu} \vdash \mathsf{ok}}

\

\noindent Recall that $\Gamma, \tilde{\mu} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\mu} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\mu}}$ and $\{\Gamma, \tilde{\mu} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\mu}}$. By IH(1) and (2), we know $F(\Gamma), F(\tilde{\mu}) \vdash F(T):F(\kappa)$ 
and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(t_j): F(T_j)\}_{(F(t_j):F(T_j)) \in F(\tilde{\mu})}$ and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(T_j): F(\kappa_j)\}_{(F(T_j):F(\kappa_j)) \in F(\tilde{\mu})}$. So we have $F(\Gamma) \vdash F(\mu T) \equiv G(\mu)F(T): F(\kappa)$ by the kinding rule in \fomega. Note that $G(\mu) \equiv |F(\tilde{\mu})|$, where $|\cdot|$ deletes all the type annotations.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \iota x.T : *}{\Gamma,
x:\iota x.T \vdash T : * }

\

\noindent By IH(1), we know $F(\Gamma), x:F(T) \vdash F(T) : *$. Since $x \notin \mathsf{FV}(F(T))$, we have $F(\Gamma) \vdash F(T):*$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \lambda X.T: \zeta X:\kappa. \kappa'}{\Gamma, X:\kappa \vdash T : \kappa' & \Gamma \vdash \kappa : \Box }

\

\noindent By IH(1), we know $F(\Gamma), X:F(\kappa) \vdash F(T) : F(\kappa')$. So $F(\Gamma) \vdash \lambda X.F(T): F(\kappa) \to F(\kappa')$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \lambda x.T: \xi x:T'.\kappa}{\Gamma, x:T' \vdash T : \kappa & \Gamma \vdash T':*}

\

\noindent By IH(1), we have $F(\Gamma), x:F(T') \vdash F(T ): F(\kappa)$. Since $x \notin \mathsf{FV}(F(T))$, we know $F(\Gamma) \vdash F(T ): F(\kappa)$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash S t: [t/x]\kappa}{\Gamma \vdash S: \xi x:T.\kappa & 
\Gamma \vdash t:T}

\

\noindent By IH(1), we have $F(\Gamma) \vdash F(S): F(\kappa)$. Then we use the fact that $F(\kappa) \equiv F([t/x]\kappa)$. 

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash S T: [T/X]\kappa}{\Gamma \vdash S: \zeta X:\kappa'.\kappa & 
\Gamma \vdash T:\kappa'}

\

\noindent By IH(1), we have $F(\Gamma) \vdash F(S):F(\kappa')\to F(\kappa)$ and $F(\Gamma) \vdash F(T):F(\kappa')$. So $F(\Gamma) \vdash F(S) F(T) : F(\kappa)$. Then we use the fact that
$F([T/X]\kappa) \equiv F(\kappa)$.

\

\noindent \textbf{Step Case}: 

\

\infer{\Gamma \vdash \forall x:T_1.T_2 : *}{ \Gamma, x:T_1 \vdash T_2 : * &
\Gamma \vdash T_1 : *}

\

\noindent By IH(1), we know $F(\Gamma), x:F(T_1) \vdash F(T_2) : *$. Since $x \notin \mathsf{FV}(F(T_2))$, we have $F(\Gamma) \vdash F(T_2) : *$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Conv}]{\Gamma \vdash t : T_2}{\Gamma \vdash t:
T_1 & \Gamma \vdash T_1 \cong T_2 & \Gamma \vdash T_2:*}

\

\noindent By lemma \ref{inj} and IH(2).

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{SelfGen}]{\Gamma \vdash t : \iota x.T}{\Gamma
\vdash t: [t/x]T & \Gamma \vdash \iota x.T: *}

\

\noindent By IH(2) and lemma \ref{subst}, we know $F(\Gamma) \vdash F(t): F(T)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{SelfInst}]{\Gamma \vdash t: [t/x]T}{\Gamma
\vdash t : \iota x.T}

\

\noindent By IH(2) and lemma \ref{subst}, we know $F(\Gamma) \vdash F(t): F(T)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Indx}]{\Gamma \vdash t : \forall x:T_1.T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:* & x \notin \mathsf{FV}(t)}

\

\noindent By IH(2), we know $F(\Gamma), x:F(T_1) \vdash F(t): F(T_2)$. Since $x \notin \mathsf{FV}(t)$, thus $x \notin \mathsf{FV}(F(t))$, so we get $F(\Gamma) \vdash F(t): F(T_2)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Dex}]{\Gamma \vdash t :[t'/x]T_2}{\Gamma
\vdash t: \forall x:T_1.T_2 & \Gamma \vdash t': T_1}

\

\noindent By IH(2) and lemma \ref{subst}, we know $F(\Gamma) \vdash F(t): F(T_2)$. 

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Mu}]{\Gamma \vdash \mu t: \mu T}{\Gamma, \tilde{\mu}
\vdash t:T &  \Gamma, \tilde{\mu} \vdash \mathsf{ok}}

\

\noindent Recall that $\Gamma, \tilde{\mu} \vdash \mathsf{ok}$ stands for $\{\Gamma, \tilde{\mu} \vdash t_j: T_j\}_{(t_j:T_j) \in \tilde{\mu}}$ and $\{\Gamma, \tilde{\mu} \vdash T_j: \kappa_j\}_{(T_j:\kappa_j) \in \tilde{\mu}}$. By (1), IH(2), we know $F(\Gamma), F(\tilde{\mu}) \vdash F(t):F(T)$ 
and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(t_j): F(T_j)\}_{(F(t_j):F(T_j)) \in F(\tilde{\mu})}$ and $\{F(\Gamma), F(\tilde{\mu}) \vdash F(T_j): F(\kappa_j)\}_{(F(T_j):F(\kappa_j)) \in F(\tilde{\mu})}$. So we have $F(\Gamma) \vdash G(\mu)F(t) \equiv F(\mu t): F(\mu T) \equiv G(\mu)F(T)$ by the rule in \fomega. Note that $G(\mu) \equiv |F(\tilde{\mu})|$, where $|\cdot|$ deletes all the type annotations.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Poly}]{\Gamma \vdash  t :\Delta X:\kappa.T}
{\Gamma, X:\kappa \vdash t: T & \Gamma \vdash \kappa:\Box}

\

\noindent By IH(2), we know $F(\Gamma), X:F(\kappa) \vdash F(t):F(T)$, so $F(\Gamma) \vdash  F(t) :\Delta X:F(\kappa).F(T)$.

\

\noindent \textbf{Step Case}: 

\


\infer[\textit{Inst}]{\Gamma \vdash t:[T'/X]T}{\Gamma \vdash t: \Delta X:\kappa.T 
& \Gamma \vdash T': \kappa}

\

\noindent By IH(2) and (1), we know $F(\Gamma) \vdash  F(t) :\Delta X:F(\kappa).F(T)$ and $F(\Gamma) \vdash F(T'):F(\kappa)$. So $F(\Gamma) \vdash  F(t) : [F(T')/X]F(T) \equiv F([T'/X]T)$(lemma \ref{subst}).

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{Func}]{\Gamma \vdash \lambda x.t : \Pi x:T_1. T_2}
{\Gamma, x:T_1 \vdash t: T_2 & \Gamma \vdash T_1:*}

\

\noindent By IH(2) and (1), we know $F(\Gamma), x:F(T_1) \vdash F(t): F(T_2)$ and $F(\Gamma) \vdash F(T_1):*$. So $F(\Gamma) \vdash \lambda x.F(t) \equiv F(\lambda x.t): F(T_1) \to F(T_2) \equiv F(\Pi x:T_1. T_2)$.

\

\noindent \textbf{Step Case}: 

\

\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t: \Pi x:T_1. T_2 & \Gamma \vdash t': T_1}

\

\noindent By IH(2), we have $F(\Gamma) \vdash F(t):F(T_1)\to F(T_2) $ and $ F(\Gamma) \vdash F(t'): F(T_1)$. So $F(\Gamma) \vdash F(t t') \equiv F(t)F(t'): F(T_2) \equiv F([t'/x]T_2)$(lemma \ref{subst}).

\end{proof}

\section{Examples}

\noindent Let $\tilde{\mu}_c$ be the following recursive defintions:

\noindent $(\mathsf{Nat}:* ) \mapsto \iota x. \Delta C: (\xi x:\mathsf{Nat}. *).  (\forall n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n))) \to (C\ 0) \to (C\ x)$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ (n\ s\ z)$

\noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$

\

\noindent Now we can see $F(\tilde{\mu}_c)$: 

\noindent $(\mathsf{Nat}:* ) \mapsto \Delta C:*.  (C \to C) \to C \to C$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ (n\ s\ z)$

\noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$

\

\noindent Let $\tilde{\mu}_s$ be the following recursive defintions:

\noindent $(\mathsf{Nat}:* ) \mapsto \iota x. \Delta C: (\xi x:\mathsf{Nat}.*).  (\Pi n : \mathsf{Nat}.C\ (\mathsf{S}\ n)) \to (C\ 0) \to (C\ x)$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ n$

\noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$

\

\noindent Then $F(\tilde{\mu}_s)$: 

\noindent $(\mathsf{Nat}:* ) \mapsto \Delta C:*.  (\mathsf{Nat} \to C) \to C \to C$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ n$

\noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$

\

\noindent Let $\tilde{\mu}_{cs}$ be the following recursive defintions:

\noindent $(\mathsf{Nat}:* ) \mapsto \iota x. \Delta C: (\xi x:\mathsf{Nat}. *).  (\Pi n : \mathsf{Nat}. (C\ n) \to (C\ (\mathsf{S}\ n))) \to (C\ 0) \to (C\ x)$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ n\ (n\ s\ z)$

\noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$

\

\noindent Then $F(\tilde{\mu}_{cs})$: 

\noindent $(\mathsf{Nat}:* ) \mapsto  \Delta C:*.  (\mathsf{Nat} \to C \to C) \to C \to C$

\noindent $(\mathsf{S}: \mathsf{Nat} \to \mathsf{Nat} )\mapsto \lambda n. \lambda s.\lambda z. s \ n\ (n\ s\ z)$

\noindent $(0:\mathsf{Nat})  \mapsto \lambda s. \lambda z.z$

\section{Type Preservation for $\mathbf{S}$}

\subsection{Confluence Analysis}

\begin{definition}[Type Reduction]
\

\noindent  $\Gamma \vdash T_1 \to_{\iota} T_2 $ if $T_1 \equiv \iota x.T' $ and $T_2 \equiv [t/x]T' $ for some fix $t \in \mathcal{M}_s$. 
\end{definition}

\begin{theorem}[Foundamental Theorem]
\label{conf}
  $\to_{o} \cup \to_{\iota} \cup \to_{\beta} \cup \to_{\mu}$ is confluent.
\end{theorem}
\begin{proof}
  We will have to refer to the $\mathsf{Selfstar}$ paper for the proof of this theorem. Informally, the $\to_{\beta}, \to_{\mu}, \to_o, \to_{\iota}$ reductions in $\mathbf{S}$ are essentially same as the ones in $\mathsf{Selfstar}$, with only the differences that in $\mathsf{S}$, we distinguish
terms, types and kinds.  
\end{proof}

\begin{definition}[Type Equivalence]
  $([\Gamma], T) =_{\mu, \beta,o,\iota} ([\Gamma], T')$ if $\Gamma \vdash T =_{\mu, \beta,o,\iota} T'$ and $\Gamma \vdash T:*$ and $\Gamma \vdash T':*$.
\end{definition}


 
\subsection{Morph Analysis}

%% Let $\Delta$ be a list representation of set $\{x_i:T_i\}_{i\in M} \cup \{X_i:\kappa_i\}_{i\in N}$
%% %% such that if $\Gamma \vdash \mathsf{wf}$, then $\Gamma, \Delta \vdash \mathsf{wf}$
%% \footnote{Note that $\Delta$ also used as binder for $\Delta X:\kappa.T$, but we do not see any ambiguities arise with the use of $\Delta$ in this article}. $\Gamma - \Delta$ means there
%% exist a $\Gamma'$ such that $\Gamma = \Gamma', \Delta$ and $\Gamma' = \Gamma - \Delta$. 

\begin{definition}[Morphing Relation]
\

  \begin{itemize}
  \item $([\Gamma], T_1) \to_{i} ([\Gamma], T_2)$ if $T_1 \equiv \Delta X:\kappa.T' $ and $T_2 \equiv [T/X]T' $ for some $T$ such that $\Gamma \vdash T:\kappa$. 
  \item $([\Gamma,X:\kappa], T_1) \to_{g} ([\Gamma], T_2) $ if $T_2 \equiv \Delta X:\kappa.T_1$ and $\Gamma \vdash \kappa:\Box$.
  \item $([\Gamma], T_1) \to_{I} ([\Gamma], T_2) $ if $T_1 \equiv \forall x:T.T' $ and $T_2 \equiv [t/x]T' $ for some $t$ such that $\Gamma \vdash t:T$. 
  \item $([\Gamma, x:T], T_1) \to_{G} ([\Gamma], T_2) $ if $T_2 \equiv \forall x:T.T_1 $ and $\Gamma \vdash T:*$. 

  \end{itemize}
\end{definition}

\begin{definition}
\

  \begin{tabular}{llll}
  $E(\Delta X:\kappa.T) := E(T)$
&
  $E(X) := X$

&

 $E(\Pi x:T_1. T_2) := \Pi x:T_1. T_2$

&
$E(\lambda X.T) := \lambda X.T$

\\

$E(T_1 T_2) := T_1 T_2$
&

$E(\forall x:T'.T) := \forall x:T'.T$
&
$E(\iota x.T) := \iota x.T$

&
$E( T \ t) := T \ t$

\\
$E(\lambda x.T) := \lambda x.T$

&

$E(\mu T) := \mu T$

\end{tabular}
\end{definition}

\begin{definition}
\

  \begin{tabular}{llll}
  $G(\Delta X:\kappa.T) := \Delta X:\kappa.T$
&
  $G(X) := X$

&

 $G(\Pi x:T_1. T_2) := \Pi x:T_1. T_2$

&
$G(\lambda X.T) := \lambda X.T$

\\

$G(T_1 T_2) := T_1 T_2$
&

$G(\forall x:T'.T) := G(T)$
&
$G(\iota x.T) := \iota x.T$

&
$G( T \ t) := T \ t$

\\
$G(\lambda x.T) := \lambda x.T$

&

$G(\mu T) := \mu T$
\end{tabular}
\end{definition}


\begin{lemma}
\label{sub}
  $E([T'/X]T) \equiv [T''/X]E(T)$ for some $T''$; $G([t/x]T) \equiv [t/x]G(T)$ .
\end{lemma}
\begin{proof}
  By induction on the structure of $T$.
\end{proof}

\begin{lemma}
\label{igelim}
  If $([\Gamma], T) {\to_{i,g}^*} ([\Gamma'],T')$, then there exist a type substitution $\sigma$ such that $\sigma E(T) \equiv E(T')$. 
\end{lemma}
\begin{proof}
  It suffices to consider $([\Gamma],T) {\to_{i,g}} ([\Gamma'], T')$.
If $T' \equiv \Delta X:\kappa .T$ and $\Gamma = \Gamma',X:\kappa$, then $E(T') \equiv E(T)$.
If $T \equiv \Delta X:\kappa .T_1$ and $T' \equiv [T''/X]T_1$ and $\Gamma = \Gamma'$, then $E(T) \equiv E(T_1)$. By lemma \ref{sub} above, we know $E(T') \equiv E([T''/X]T_1) \equiv [T_2/X]E(T_1)$ for some $T_2$. 
\end{proof}


\begin{lemma}
\label{IGelim}
  If $([\Gamma], T) {\to_{I,G}^*} ([\Gamma'], T')$, then there exist a term substitution $\delta$ such that $\delta G(T) \equiv G(T')$. 
\end{lemma}
\begin{proof}
  It suffices to consider $([\Gamma], T) {\to_{I,G}} ([\Gamma'], T')$.
If $T' \equiv \forall x:T_1 .T$ and $\Gamma = \Gamma',x:T_1$, then $G(T') \equiv G(T)$.
If $T \equiv \forall x:T_2 .T_1$ and $T' \equiv [t/x]T_1$ and $\Gamma = \Gamma'$, then $E(T) \equiv E(T_1)$. By lemma \ref{sub} above, we know $E(T') \equiv E([t/x]T_1) \equiv [t/x]E(T_1)$. 
\end{proof}

\begin{lemma}
\label{typesub}
  If $([\Gamma],\Pi x:T_1. T_2) {\to_{i,g}^*} ([\Gamma'], \Pi x:T_1'.T_2')$, then there exist a type substitution $\sigma$ such that $\sigma(\Pi x:T_1.T_2) \equiv \Pi x:T_1'.T_2'$.
\end{lemma}

\begin{proof}
  By lemma \ref{igelim} above.
\end{proof}

\begin{lemma}
\label{termsub}
  If $([\Gamma], \Pi x:T_1. T_2) {\to_{I,G}^*} ([\Gamma'], \Pi x:T_1'.T_2')$, then there exist a term substitution $\delta$ such that $\delta(\Pi x:T_1.T_2) \equiv \Pi x:T_1'.T_2'$.
\end{lemma}

\begin{proof}
  By lemma \ref{IGelim} above.
\end{proof}

\noindent Let $\to_{o,\iota,\beta,\mu,i,g,I,G}^*$ denote $(\to_{i,g,I,G} \cup =_{o,\iota,\beta,\mu})^*$.
Let $\to_{o,\iota,\beta,\mu,i,g,I,G}$ denote $\to_{i,g,I,G} \cup =_{o,\iota,\beta,\mu}$.
\begin{theorem}[Compatibility]
\label{comp}
  If $([\Gamma], \Pi x:T_1. T_2)  \to_{o,\iota,\beta,\mu,i,g,I,G}^* ([\Gamma'],\Pi x:T_1'. T_2')$, then there exist a mixed substitution $\phi$ such that $([\Gamma], \phi(\Pi x:T_1. T_2)) =_{o,\iota,\beta,\mu} ([\Gamma],\Pi x:T_1'.T_2')$. Thus $\Gamma \vdash \phi T_1 =_{o,\beta,\mu} T_1'$ and $\Gamma \vdash \phi T_2 =_{o,\beta,\mu} T_2'$(theorem \ref{conf}).
\end{theorem}
\begin{proof}
By lemma \ref{termsub} and lemma \ref{typesub}. And we make use of the fact that if $\Gamma \vdash t =_{o,\iota,\beta,\mu} t'$, then for any mixed
substitution $\phi$, we have $\Gamma \vdash \phi t =_{o,\iota,\beta,\mu} \phi t'$.
\end{proof}

\subsection{Type Preservation}

\begin{lemma}
\label{type}
  Let $([\Gamma, \Delta], T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}}^* ([\Gamma], T_2)$. If $\Gamma, \Delta \vdash t:T_1$ with $\mathsf{dom}(\Delta) \# \mathsf{FV}(t)$, then $\Gamma \vdash t:T_2$. 
\end{lemma}

\noindent \textbf{Note}: We write $\stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G}$ to means
the same thing as ${\to}_{\beta,\mu,\iota,o, i, g, I, G}^*$ with an emphasis on the subject $t$. 

\begin{lemma} 
\label{conv}
 If $([\Gamma], T_1) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma'],T_2)$ and $\Gamma \vdash t =_{\beta,\mu} t'$, then $([\Gamma], T_1) \stackrel{t'}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma'],T_2)$.  
\end{lemma} 
\begin{proof} By induction on length of $([\Gamma],T_1) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i,g, I, G} ([\Gamma],T_2)$. Note that this lemma is \textbf{not} subject expansion, do not get confused.
\end{proof}


\begin{lemma} 
    \label{perm} If $\Gamma, \tilde{\mu}, y:T'
\vdash t:T$ , then $\Gamma, y: \mu  T',\tilde{\mu} 
 \vdash t :T$.  
 \end{lemma}
\begin{proof} By induction on the
derivation of $\Gamma, \tilde{\mu} , y:T' \vdash t:T$.
\end{proof}

\noindent \textbf{Note}: If $\Delta = x:T,..., X:\kappa$, then $\mu \Delta := x:\mu T,..., X:\mu \kappa$. 

\begin{lemma} 
    \label{metacong} 
    If $([\Gamma, \tilde{\mu}, \Delta], T) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}, \Delta'], T')$ for some $\Delta, \Delta'$ and $\Gamma, \mu \Delta , \tilde{\mu}
\vdash \mathsf{ok}$, then 

\noindent $([\Gamma, \mu \Delta], \mu T) \stackrel{\mu t }{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \mu \Delta'], \mu T')$.
 \end{lemma} 
 \begin{proof} By induction on length of $([\Gamma, \tilde{\mu}, \Delta], T) \stackrel{t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}, \Delta'], T')$. We list a few cases.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta],T) {=_{\beta,\mu, o}} ([\Gamma, \tilde{\mu}, \Delta],T')$.

\

\noindent Use lemma \ref{perm}, we have $([\Gamma, \mu \Delta], \mu T)   =_{\beta,\mu,o}  ([\Gamma , \mu \Delta'], \mu T')$. 

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta], \iota x.T) {=_{\iota}} ([\Gamma, \tilde{\mu}, \Delta], [t/x]T)$. 

\

\noindent We know $([\Gamma, \mu \Delta] , \mu \iota x.T ) {=_{\mu}} ( [\Gamma, \mu \Delta],\iota x.\mu T)  {=_{\iota}}([\Gamma, \mu \Delta], [\mu t/x] \mu T) {=_{\mu}} ([\Gamma, \mu \Delta], \mu [t/x]T)$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta], \Delta X:\kappa.T) {\to_{i}} ([\Gamma, \tilde{\mu}, \Delta],[T'/X]T)$ with $\Gamma, \tilde{\mu}, \Delta \vdash T':\kappa$.

\

\noindent We know $([\Gamma, \mu \Delta], \mu (\Delta X:\kappa.T)) {=_{\mu}} ([\Gamma, \mu \Delta], \Delta X:\mu \kappa.\mu T)  {\to_{i}} ([\Gamma, \mu \Delta],[\mu T'/X] \mu T) {=_{\mu}} ([\Gamma, \mu \Delta], \mu ([T'/X]T))$ with $\Gamma, \mu\Delta \vdash \mu T': \mu \kappa$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta, X:\kappa],T) {\to_{g}} ([\Gamma, \tilde{\mu}, \Delta],\Delta X:\kappa.T)$ with $\Gamma, \tilde{\mu},\Delta \vdash \kappa:\Box$.

\

\noindent We know $([\Gamma, \mu \Delta, X: \mu \kappa],\mu T)  {\to_{g}} ([\Gamma, \mu\Delta], \Delta X:\mu \kappa. \mu T) {=_{\mu}} ([\Gamma, \mu\Delta], \mu (\Delta X:\kappa.T))$ with $\Gamma, \mu\Delta \vdash \mu \kappa:\Box$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta], \forall x:T'.T) {\to_{I}} ([\Gamma, \tilde{\mu}, \Delta], [t/x]T)$ with $\Gamma, \tilde{\mu}, \Delta \vdash t:T'$.

\

\noindent We know $([\Gamma, \mu \Delta],\mu(\forall x:T'.T)) {=_{\mu}} ([\Gamma, \mu \Delta], \forall x:\mu T'.\mu T)  {\to_{I}} ([\Gamma, \mu \Delta],[\mu t/x] \mu T) {=_{\mu}}([\Gamma, \mu \Delta], \mu [t/x]T)$ with $\Gamma,\mu\Delta \vdash \mu t: \mu T'$.

\

\noindent\textbf{Case}: $([\Gamma, \tilde{\mu}, \Delta, x:T'], T) {\to_{G}} ([\Gamma, \tilde{\mu}, \Delta], \forall x:T'.T)$ with $\Gamma, \tilde{\mu}, \Delta \vdash T':*$.

\

\noindent We know $([\Gamma, \mu \Delta, x:\mu T'],\mu T)  {\to_{G}}([\Gamma, \mu \Delta], \forall x:\mu T'. \mu T) {=_{\mu}} ([\Gamma, \mu \Delta],\mu (\forall x:T'.T))$ with $\Gamma, \mu \Delta \vdash \mu T':*$.


\end{proof}

\begin{lemma}[Inversion I]
If $\Gamma \vdash x:T$, then exist a $\Delta, T_1$ such that $([\Gamma, \Delta], T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], T)$ and $(x:T_1) \in \Gamma$.
\end{lemma}

\begin{lemma}[Inversion II]
If $\Gamma \vdash t_1 t_2:T$, then exist $\Delta, T_1, T_2$ such that $\Gamma, \Delta \vdash t_1:\Pi x:T_1.T_2$ and $\Gamma, \Delta \vdash t_2:T_1$ and $([\Gamma, \Delta], [t_2/x]T_2) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma],T)$. 
\end{lemma}

\begin{lemma}[Inversion III]
If $\Gamma \vdash \lambda x.t:T$, then exist $\Delta, T_1, T_2$ such that $\Gamma, \Delta , x:T_1 \vdash t:T_2$ and $([\Gamma, \Delta], \Pi x:T_1. T_2) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], T)$. 
\end{lemma}

\begin{lemma}[Inversion IV]
If $\Gamma \vdash \mu t:T$, then exist $\Delta, T_1$ such that $\Gamma, \Delta, \tilde{\mu} \vdash t:T_1$ and $([\Gamma, \Delta], \mu T_1) {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma],T)$.
\end{lemma}


\begin{lemma}[Substitution]
\label{subst}
\

  \begin{enumerate}
  \item   If $\Gamma \vdash t:T$, then for any mixed substitution $\phi$ with $\mathsf{dom}(\phi) \# \mathsf{FV}(t) $, $\phi \Gamma \vdash t: \phi T$.
\item If $\Gamma, x:T \vdash t:T'$ and $\Gamma \vdash t':T$, then $\Gamma \vdash [t'/x]t:[t'/x]T'$.
  \end{enumerate}

\end{lemma}

\begin{proof}
  By induction on derivation.
\end{proof}

\begin{theorem}
  If $\Gamma \vdash t:T$ and $\Gamma \vdash t \to_{\beta, \mu} t'$ and $\Gamma \vdash \mathsf{wf}$, then $\Gamma \vdash t':T$.
\end{theorem}
\begin{proof}
  By induction on derivation of $\Gamma \vdash t:T$. We list a few interesting 
cases.

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash x:T}{ x:T \in \Gamma}

\

\noindent If $\Gamma \vdash x \to_{\beta} t'$, this means $ (x:T) \mapsto t'
\in \Gamma$ and $\Gamma \vdash t':T$ since $\Gamma \vdash \mathsf{wf}$.

\

\noindent \textbf{Case}:

\

\infer[\textit{App}]{\Gamma \vdash t t':[t'/x]T_2}{\Gamma
\vdash t:\Pi x:T_1.T_2 & \Gamma \vdash t': T_1}

\

\noindent Suppose $\Gamma \vdash (\lambda x.t_1) t_2 \to_{\beta} [t_2/x]t_1$. We know that
$\Gamma \vdash \lambda x.t_1 : \Pi x:T_1. T_2$ and $\Gamma \vdash t_2:T_1$. By
inversion on $\Gamma \vdash \lambda x.t_1 : \Pi x:T_1. T_2$, we know that 
there exist $\Delta, T_1', T_2'$ such that $\Gamma, \Delta, x:T_1' \vdash t_1:T_2'$
and $([\Gamma, \Delta], \Pi x:T_1'.T_2') {\to_{o,\iota,\beta,\mu,i,g,I,G}^*} ([\Gamma], \Pi x:T_1.T_2)$. 
By theorem \ref{comp}, we have $([\Gamma, \Delta], \phi(\Pi x:T_1'.T_2')) =_{o,\iota,\beta,\mu} ([\Gamma, \Delta],\Pi x:T_1. T_2)$. By Church-Rosser
of $=_{o,\iota,\beta,\mu}$, we have $\Gamma, \Delta \vdash \phi T_1'=_{o,\beta,\mu}  T_1$ and $\Gamma, \Delta \vdash \phi T_2' =_{o,\beta,\mu} T_2$. 
So by (1) of lemma \ref{subst}, we have $\Gamma,\phi(\Delta), x:\phi T_1' \vdash t_1: \phi T_2'$ with $\mathsf{dom}(\phi(\Delta)) \# \mathsf{FV}(\phi T_1') \cup \mathsf{FV}(\phi T_2') \cup \mathsf{FV}(t_1) $. So $\Gamma,\phi(\Delta), x: T_1 \vdash t_1: T_2$. Since $\Gamma \vdash t_2:T_1$, by (2) of lemma \ref{subst}, $\Gamma, \phi(\Delta) \vdash [t_2/x]t_1: [t_2/x]T_2$. So we have $\Gamma\vdash [t_2/x]t_1: [t_2/x]T_2$. 

\

\noindent \textbf{Case:}

\

\infer{\Gamma \vdash \mu t: \mu T}{\Gamma, \tilde{\mu}
\vdash t:T &  \Gamma, \tilde{\mu} \vdash \mathsf{ok} }

\

\noindent Suppose  $\Gamma \vdash \mu x_j \to_{\beta} \mu
t_j$, where $x_j \mapsto t_j \in \mu$. We have $\Gamma, \tilde{\mu} \vdash x_j:T$. By
inversion, $\Gamma, \tilde{\mu}, \Delta \vdash x_j:T_j$ and $([\Gamma, \tilde{\mu}, \Delta], T_j) \stackrel{x_j}{\to}_{\beta,\mu,\iota,o, i,g,I,G}  ([\Gamma, \tilde{\mu}], T)$. 
 Since $\Gamma, \tilde{\mu}, \Delta \vdash x_j =_{\beta} t_j$ and by lemma \ref{conv}, we   
get $([\Gamma, \tilde{\mu} , \Delta],T_j) \stackrel{t_j}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}],T)$. 
Since $\Gamma, \tilde{\mu}, \Delta \vdash  t_j : T_j$, by lemma \ref{type}, $\Gamma, \tilde{\mu}\vdash t_j:T$. Thus we have $\Gamma \vdash \mu t_j : \mu T$.

\

\noindent Suppose  $\Gamma\vdash \mu t \to_{\mu} t$, where $\mathsf{FV}(t) \# \mathsf{dom}(\mu)$. 
We have $\Gamma, \tilde{\mu} \vdash t : T$ and $\mathsf{FV}(t)\cup \mathsf{FV}(T) \# \mathsf{dom} (\mu)$. So we have $([\Gamma],\mu T)  {=}_{\mu} ([\Gamma], T)$. We also know that $\Gamma \vdash t : T$, so $\Gamma
\vdash t : \mu T$(lemma \ref{type}).

\

\noindent Suppose $\Gamma\vdash \mu \lambda x.t \to_{\mu} \lambda  x. \mu  t$. We have $\Gamma, \tilde{\mu} \vdash \lambda  x.t : T$ and 
$\Gamma, \tilde{\mu}, \Delta, x:T_1 \vdash t : T_2$ and $([\Gamma, \tilde{\mu}, \Delta],
\Pi  x:T_1.T_2) \stackrel{\lambda  x.t}{\to}_{\beta,\mu,\iota,o, i,g, I, G}  ([\Gamma, \tilde{\mu}],T)$(by inversion). Thus we have $\Gamma, \mu \Delta, x:\mu T_1 \vdash \mu
  t: \mu   T_2$(lemma \ref{perm}) and
$([\Gamma, \mu \Delta], \mu(\Pi  x:T_1.T_2)) \stackrel{\mu
 \lambda  x.t}{\to}_{\beta,\mu,\iota,o, i,g, I, G} ([\Gamma], \mu  T)$(lemma \ref{metacong}). By lemma \ref{conv}, $([\Gamma, \mu \Delta], (\Pi  x:\mu  T_1.\mu  T_2))
\stackrel{\lambda  x.\mu  t}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma], \mu  T)$. 
Also, $\Gamma, \mu \Delta \vdash \lambda  x.\mu t : \Pi  x: (\mu  T_1).(\mu T_2)$.  
So by lemma \ref{type}, $\Gamma \vdash \lambda x.\mu   t :  \mu  T$.

\

\noindent Suppose $\Gamma\vdash \mu  (t_1' t_2') \to_{\mu} (\mu  t_1')( \mu  t_2')$. We have $\Gamma, \tilde{\mu} \vdash t_1't_2' : T $ and $\Gamma, \tilde{\mu}, \Delta \vdash t_1' : \Pi  x:T_1. T_2$ and $\Gamma, \tilde{\mu}, \Delta \vdash t_2' : T_1$ and $([\Gamma, \tilde{\mu}, \Delta], [t_2'/x]T_2) \stackrel{t_1't_2'}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma, \tilde{\mu}], T)$(by inversion). Thus we have $\Gamma , \mu \Delta \vdash \mu   t_1':  \mu  (\Pi x:T_1.T_2)$ and $\Gamma, \mu \Delta \vdash \mu   t_2':  \mu T_1$ and $([\Gamma, \mu \Delta], \mu ([t_2'/x]T_2)) \stackrel{\mu  (t_1' t_2')}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma],\mu T) $(lemma \ref{metacong}). By
lemma \ref{conv}, we have $([\Gamma, \mu \Delta], \mu ([t_2'/x]T_2)) \stackrel{(\mu t_1')(\mu t_2')}{\to}_{\beta,\mu,\iota,o, i, g, I, G} ([\Gamma],\mu T) $. So $\Gamma, \mu \Delta \vdash
(\mu   t_1')(\mu   t_2') :[\mu t_2'/x]\mu  T_2$ and then $\Gamma \vdash (\mu   t_1')(\mu   t_2') : \mu T$(lemma \ref{type}).

\end{proof}


\noindent Cite \cite{Girard:1989}.
\bibliographystyle{plain}
\bibliography{real}

\end{document}
